COMMENT ⊗   VALID 00012 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	AUX:<CL.THM>BASIS.LISP.0
C00019 00003	AUX:<CL.THM>GENFACT.LISP.0
C00020 00004	AUX:<CL.THM>EVENTS.LISP.0
C00021 00005	AUX:<CL.THM>CODE-1-A.LISP.0
C00025 00006	AUX:<CL.THM>CODE-B-D.LISP.0
C00030 00007	AUX:<CL.THM>CODE-E-M.LISP.0
C00036 00008	AUX:<CL.THM>CODE-N-R.LISP.0
C00042 00009	AUX:<CL.THM>CODE-S-Z.LISP.0
C00047 00010	AUX:<CL.THM>IO.LISP.0
C00048 00011	AUX:<CL.THM>PPR.LISP.0
C00049 00012	AUX:<CL.THM>TOPS-20-EMACS-TO-THM.LISP.0
C00050 ENDMK
C⊗;
AUX:<CL.THM>BASIS.LISP.0
10741,MACLISP
(DEFUN SHARP-OPEN 6411
(DEFMACRO DEFCONST 8237
(DEFMACRO DEFVAR 8390
(DEFMACRO DEFCONSTANT 8658
(DEFCONST THEOREM-PROVER-FILES8804
(DEFMACRO LOGNOT 9072
(DEFMACRO LOGAND 9125
(DEFUN AN-ERROR 9703
(DEFMACRO OUR-EXPLODEC 10110
(DEFMACRO OUR-EXPLODEN 10282
(DEFMACRO OUR-GETCHAR 10447
(DEFMACRO OUR-GETCHARN 10553
(DEFMACRO OUR-IMPLODE 10651
(DEFMACRO TP-EXPLODEN 11465
(DEFMACRO TP-GETCHARN 11565
(DEFMACRO TP-IMPLODE 11672
(DEFUN HERALD 12152
(DEFUN HERALD 12200
(DEFCONST ALPHABETIC-CASE-AFFECTS-STRING-COMPARISON 12447
(DEFCONSTANT EVENT-SEPARATOR-STRING 12489
(DEFCONSTANT KEYWORD-BREAK 12535
(DEFCONSTANT KEYWORD-IN 12590
(DEFCONSTANT KEYWORD-OUT 12640
(DEFVAR LIB-FILE)12684
(DEFVAR LIB-VARS)12705
(DEFVAR LIB-ATOMS-WITH-PROPS)12738
(DEFVAR LIB-ATOMS-WITH-DEFS)12770
(DEFVAR LIB-PROPS)12792
(DEFCONST LINEL-VALUE 13031
(DEFCONST PROVE-FILE 13059
(DEFCONST STANDARD-RANDSET 13393
(DEFMACRO DEFEVENT 13659
(DEFMACRO GET0 14678
(DEFMACRO GET1 14758
(DEFMACRO NEQ 14846
(DEFMACRO PAIRP 14912
(DEFUN ALPHORDER 15252
(DEFUN CHAR-EQUAL 15480
(DEFUN CHAR-IN-STRING 15710
(DEFUN CHAR-UPCASE 15854
(DEFUN CLOSE? 15944
(DEFUN COMPILE-IF-APPROPRIATE-AND-POSSIBLE 16294
(DEFUN COPYLIST 17237
(DEFUN COPYTREE 17293
(DEFUN EXTEND-FILE-NAME 17389
(DEFUN FIND-CHAR-IN-FILE 17817
(DEFUN FIND-STRING-IN-FILE 18841
(DEFUN FIND-STRING-IN-STRING 19500
(DEFUN GET-TOTAL-STATS 19837
(DEFUN GET-FROM-FILE 20208
(DEFUN GET-PLIST-FROM-FILE 20390
(DEFUN GET-STATS-FILE 20634
(DEFUN GET-STATS-OLD-FILE 21297
(DEFUN GET-TAIL 21806
(DEFUN GET00 21935
(DEFUN GET11 22069
(DEFUN GETEOFPTR 22243
(DEFUN GETFILEPTR 22327
(DEFUN IDATE 22412
(DEFUN INTERSECTION 22639
(DEFUN KILL-DEFINITION 22719
(DEFUN LENGTHF 23017
(DEFUN LINEL 23396
(DEFUN MAKE-LIB 23527
(DEFUN NOTE-LIB 25762
(DEFUN OK-SYMBOLP 26498
(DEFUN OPENP 27999
(DEFUN OUR-FBOUNDP 28126
(DEFUN PACK 28255
(DEFUN EXPLODE-NUMBER 28486
(DEFUN PREPARE-FOR-THE-NIGHT 28756
(DEFUN PRINT-SYSTEM 28958
(DEFUN PRINT-DATE-LINE 29506
(DEFUN RANDOM-INITIALIZATION 29579
(DEFUN RANDOM-NUMBER 29776
(DEFUN READ-FILE 29835
(DEFUN REMQ 30063
(DEFUN REMOVE 30138
(DEFUN SETFILEPTR 30216
(DEFUN STORE-DEFINITION 30315
(DEFUN STRING-DOWNCASE 30616
(DEFUN STRING-LENGTH 30782
(DEFUN R-LOOP 30898
(DEFUN TIME-IT 31032
(DEFUN TIME-DIFFERENCE 31200
(DEFUN TIME-IN-60THS 31363
(DEFUN UNION 31830
(DEFUN XSEARCH 31920
(DEFVAR *ALIST*)32786
(DEFVAR *ARGLIST*)32808
(DEFVAR *CONTROLLER-COMPLEXITIES*)32846
(DEFVAR *FILE*)32865
(DEFVAR *FNNAME*)32886
(DEFVAR *INDENT*)32907
(DEFVAR *TYPE-ALIST*)32932
(DEFVAR 1BTM-OBJECTS)33350
(DEFCONSTANT 1F 33440
(DEFCONSTANT 1SHELL-QUOTE-MARK 33536
(DEFCONSTANT 1T 33672
(DEFVAR ABBREVIATIONS-USED)33762
(DEFVAR ADD-EQUATIONS-TO-DO)33898
(DEFCONST ADD-TERM-TO-POT-LST-TEMP 34048
(DEFVAR ALIST)34113
(DEFVAR ALISTS)34132
(DEFVAR ALL-FNS-FLG)34156
(DEFCONST ALL-LEMMAS-USED 34186
(DEFCONST ALMOST-SUBSUMES-CONSTANT 34229
(DEFVAR ALMOST-SUBSUMES-LITERAL)34703
(DEFCONST ANCESTORS 34778
(DEFVAR ANS)35152
(DEFVAR ARGS)35299
(DEFCONST ARITY-ALIST 35325
(DEFCONST BOOK-SYNTAX-FLG 35892
(DEFCONST BOOT-STRAP-INSTRS36109
(DEFCONST BOOT-STRAP-MACRO-FNS 44995
(DEFCONST BROKEN-LEMMAS 45169
(DEFVAR CHRONOLOGY)45196
(DEFVAR CL2)45280
(DEFCONST CLAUSE-ALIST 45307
(DEFVAR COMMONSUBTERMS)45338
(DEFCONST COMMUTED-EQUALITY-FLG 45374
(DEFCONST CULPRIT-FUNCTION 45409
(DEFCONST CURRENT-ATM 45439
(DEFVAR CURRENT-CL)45677
(DEFCONST CURRENT-LIT 45775
(DEFVAR CURRENT-SIMPLIFY-CL)46102
(DEFVAR CURRENT-TYPE-NO)46130
(DEFVAR DECISIONS)46241
(DEFVAR DEFINITELY-FALSE)46270
(DEFVAR DEFN-FLG)46435
(DEFVAR DESCENDANTS)46800
(DEFVAR DISABLED-LEMMAS)46828
(DEFVAR DLHDFMLA)47019
(DEFCONST DO-NOT-USE-INDUCTION-FLG 47058
(DEFCONST DOTCONS 47191
(DEFVAR ELAPSEDTHMTIME)47233
(DEFCONST ELIM-VARIABLE-NAMES47266
(DEFCONST ELIM-VARIABLE-NAMES1 48035
(DEFVAR ENDLIST)48059
(DEFVAR EVENT-LST)48081
(DEFCONST EXECUTE-PROCESSES48112
(DEFCONST EXPAND-LST 48483
(DEFCONST FAILED-THMS 48513
(DEFVAR FAILURE-ACTION)49173
(DEFCONST FAILURE-MSG 49199
(DEFCONST FALSE 49641
(DEFVAR FALSE-TYPE-ALIST)49797
(DEFVAR FILE)49814
(DEFVAR FLATSIZE)49835
(DEFVAR FMLA)49852
(DEFVAR FNS)49868
(DEFVAR FNSTACK)49888
(DEFCONST FNS-TO-BE-IGNORED-BY-REWRITE 49931
(DEFCONST FORCEIN 50135
(DEFCONST FOR-OPS50168
(DEFVAR FORM)50355
(DEFCONST GEN-VARIABLE-NAMES 50388
(DEFVAR GEN-VARIABLE-NAMES1)50546
(DEFCONST GENERALIZE-LEMMA-NAMES 50654
(DEFVAR GENERALIZE-LEMMAS)50688
(DEFCONST GENERALIZING-SKOS 50811
(DEFVAR GENRLTLIST)50838
(DEFCONST HEURISTIC-TYPE-ALIST 50873
(DEFVAR HIGHER-PROPS)51107
(DEFCONST HINT 51250
(DEFVAR HINTS)51331
(DEFCONST HINT-VARIABLE-ALIST51480
(DEFCONST HINTED-EXPANSIONS 53043
(DEFVAR HIST-ENTRY)53180
(DEFVAR ID-IFF)53199
(DEFVAR INDENT)53218
(DEFVAR INDUCTION-CONCL-TERMS)53252
(DEFCONST INDUCTION-HYP-TERMS 53286
(DEFVAR INST-HYP)53311
(DEFCONST IN-ADD-AXIOM-FLG 53342
(DEFCONST IN-BOOT-STRAP-FLG 53378
(DEFCONST IN-REDO-UNDONE-EVENTS-FLG 53422
(DEFCONST IN-PROVE-LEMMA-FLG 53459
(DEFCONST IO-FN 53483
(DEFCONST IOTHMTIME 53779
(DEFCONST IPOSITION-ALIST 53884
(DEFVAR LAST-CLAUSE)53912
(DEFVAR LAST-EXIT)53934
(DEFVAR LAST-HYP)54046
(DEFVAR LAST-PRIN5-WORD)54157
(DEFCONST LAST-PRINEVAL-CHAR 54190
(DEFVAR LAST-PRINT-CLAUSES)54451
(DEFCONST LAST-PROCESS 54478
(DEFVAR LINEARIZE-ASSUMPTIONS-STACK)54522
(DEFCONST LEFTMARGINCHAR 54551
(DEFCONST LEMMA-DISPLAY-FLG 54690
(DEFCONST LEMMA-TYPES 54720
(DEFVAR LEMMA-STACK)54882
(DEFVAR LEMMAS-USED-BY-LINEAR)54916
(DEFVAR LINEAR-ASSUMPTIONS)55056
(DEFCONST LITATOM-FORM-COUNT-ALIST 55223
(DEFCONST LITS-THAT-MAY-BE-ASSUMED-FALSE 55272
(DEFCONST LITS-TO-BE-IGNORED-BY-LINEAR 55992
(DEFCONSTANT MAGIC-CHAR-NO 56127
(DEFVAR MAIN-EVENT-NAME)56159
(DEFVAR MARG2)56429
(DEFVAR MASTER-ROOT-NAME)56515
(DEFVAR MATCH-TEMP)56730
(DEFVAR MATCH-X)56796
(DEFCONST META-NAMES 56821
(DEFVAR MINREM)57047
(DEFCONST MUST-BE-FALSE 57075
(DEFCONST MUST-BE-TRUE 57106
(DEFVAR NAME)57127
(DEFVAR NAMES)57145
(DEFVAR NEXT-MEMO-KEY)57171
(DEFVAR NEXT-MEMO-VAL)57197
(DEFVAR NEXTIND)57217
(DEFVAR NEXTNODE)57238
(DEFCONST NILCONS 57260
(DEFCONST NO-BUILT-IN-ARITH-FLG 57311
(DEFVAR NONCONSTRUCTIVE-AXIOM-NAMES)57445
(DEFVAR NUMBER-OF-VARIABLES)57630
(DEFVAR OBJECTIVE)57652
(DEFCONST OBVIOUS-RESTRICTIONS 57687
(DEFVAR ORIG-LEMMA-STACK)57720
(DEFVAR ORIG-LINEARIZE-ASSUMPTIONS-STACK)57765
(DEFCONST ORIGEVENT 57789
(DEFVAR ORIGTHM)57813
(DEFCONSTANT PARAGRAPH-INDENT 57847
(DEFVAR PARENT)57940
(DEFVAR PARENT-HIST)57964
(DEFVAR POS)57980
(DEFCONST PPR-MACRO-LST58007
(DEFVAR PPR-MACRO-MEMO)58299
(DEFVAR PPRFILE)58319
(DEFCONST PPRFIRSTCOL 58345
(DEFCONST PPRMAXLNS 58372
(DEFCONST PRINEVAL-FNS58404
(DEFVAR PROCESS)58988
(DEFVAR PROCESS-CLAUSES)59016
(DEFVAR PROCESS-HIST)59041
(DEFVAR PROP)59058
(DEFVAR PROPLIST)59079
(DEFVAR PROVE-TERMINATION-LEMMAS-USED)59121
(DEFCONST PROVED-THMS 59147
(DEFCONST R-ALIST 59250
(DEFVAR RECOGNIZER-ALIST)59283
(DEFVAR RECORD-DECLARATIONS)59804
(DEFVAR RECORD-TEMP)59828
(DEFVAR RELIEVE-HYPS-NOT-OK-ANS)59931
(DEFVAR REMAINDER)59953
(DEFVAR SCRIBE-FLG)59976
(DEFVAR SETQ-LST)59997
(DEFVAR SHELL-ALIST)60021
(DEFVAR SHELL-POCKETS)60469
(DEFVAR SIMPLIFY-CLAUSE-MAXIMALLY-CLAUSES)60637
(DEFVAR SIMPLIFY-CLAUSE-MAXIMALLY-HIST)60680
(DEFVAR SIMPLIFY-CLAUSE-POT-LST)60716
(DEFVAR SINGLETON-TYPE-SETS)60829
(DEFVAR SPACELEFT)61272
(DEFCONST STACK 61292
(DEFVAR STARTLIST)61318
(DEFCONSTANT STRING-ONE 61346
(DEFVAR T2)61373
(DEFCONST TAB-SIZE 61396
(DEFVAR TEMP-TEMP)61421
(DEFVAR TEMP1)61517
(DEFCONST TEMPORARILY-DISABLED-LEMMAS 61559
(DEFCONST TERMS-TO-BE-IGNORED-BY-REWRITE 61608
(DEFVAR TEST-LST)61633
(DEFVAR THM)61649
(DEFCONST TRANSLATE-TO-LISP-TIME 61686
(DEFCONSTANT TREE-INDENT 61835
(DEFCONSTANT TREE-LINES 61961
(DEFCONST TRUE 62076
(DEFCONST TRUE-CLAUSE 62221
(DEFCONST TRUE-TYPE-ALIST 62369
(DEFCONST TTY-FILE 62396
(DEFCONST TYPE-ALIST 62506
(DEFCONSTANT TYPE-SET-BOOLEAN 62900
(DEFCONSTANT TYPE-SET-CONS 63031
(DEFCONSTANT TYPE-SET-FALSE 63097
(DEFCONSTANT TYPE-SET-LITATOMS 63216
(DEFCONSTANT TYPE-SET-NEGATIVES 63285
(DEFCONSTANT TYPE-SET-NUMBERS 63354
(DEFVAR TYPE-SET-TERM1)63518
(DEFCONSTANT TYPE-SET-TRUE 63549
(DEFCONSTANT TYPE-SET-UNKNOWN 63666
(DEFCONST UN-PRODUCTIVE-PROCESSES63771
(DEFCONST UNDONE-BATCH-COMMANDS 64330
(DEFVAR UNDONE-EVENTS)64360
(DEFCONST UNDONE-EVENTS-STACK 64394
(DEFVAR UNIFY-SUBST)64422
(DEFVAR UNIVERSE)64443
(DEFCONST USE-NO-LEMMAS-FLG 64475
(DEFVAR VAL)65111
(DEFVAR VAR-ALIST)65133
(DEFCONST WELL-ORDERING-RELATIONS 65171
(DEFCONST ZERO 65463
(DEFMACRO 1IF 65541
(DEFMACRO ADD-SUB-FACT-BODY 65612
(DEFMACRO ACCESS 65662
(DEFMACRO ARGN 65725
(DEFMACRO BINDINGS 65771
(DEFMACRO CHANGE 65819
(DEFMACRO DISABLEDP 65898
(DEFMACRO FARGN 66045
(DEFMACRO FARGS 66089
(DEFMACRO FCONS-TERM 66128
(DEFMACRO FCONS-TERM* 66184
(DEFMACRO FFN-SYMB 66237
(DEFMACRO FN-SYMB 66273
(DEFMACRO FQUOTEP 66321
(DEFMACRO LOGBIT 66375
(DEFMACRO LOGDIFF 66413
(DEFMACRO MAKE 66455
(DEFMACRO MATCH 66506
(DEFMACRO MATCH! 66560
(DEFMACRO NVARIABLEP 66619
(DEFMACRO PQUOTE 66656
(DEFMACRO PRIND 66692
(DEFMACRO QUOTEP 66867
(DEFMACRO SWAP 66967
(DEFMACRO TYO1 67027
(DEFMACRO TYPE-PRESCRIPTION 67117
(DEFMACRO VALUEP 67193
(DEFMACRO VARIABLEP 67234
(DEFUN 1CAR 67265
(DEFUN 1CDR 67360
(DEFUN ACCESS-MACRO 67463
(DEFUN ADD-TO-SET 68277
(DEFUN ARGN-MACRO 68355
(DEFUN BINDINGS-MACRO 68702
(DEFUN CELL 68840
(DEFUN CREATE-LEMMA-STACK 68955
(DEFUN CREATE-LINEARIZE-ASSUMPTIONS-STACK 69112
(DEFUN CREATE-STACK1 69298
(DEFUN EQLENGTH 69516
(DEFUN FARGN-MACRO 69566
(DEFUN FN-SYMB-MACRO 69754
(DEFUN GET-FIELD-NUMBER 69962
(DEFUN IPOSITION 70430
(DEFUN ITERPRI 70757
(DEFUN ITERPRIN 70827
(DEFUN ITERPRISPACES 70907
(DEFUN IPRIN1 70973
(DEFUN IPRINC 71053
(DEFUN IPRINT 71200
(DEFUN ISPACES 71283
(DEFUN KWOTE 71413
(DEFUN MAKE-MACRO 71451
(DEFUN MATCH-MACRO 72083
(DEFUN MATCH!-MACRO 72297
(DEFUN MATCH1-MACRO 72430
(DEFUN MATCH2-MACRO 72711
(DEFUN NCONC1 74205
(DEFUN RECORD-DECLARATION 74260
(DEFUN RECORD-DECLARATION-LST 75110
(DEFUN SPACES 75206
(DEFUN SPELL-NUMBER 75317
(DEFUN CHANGE-MACRO 75649
(DEFUN SUB-PAIR 76480
(DEFCONST LEMMA-STACK 83987
(DEFCONST LINEARIZE-ASSUMPTIONS-STACK84072
∨
AUX:<CL.THM>GENFACT.LISP.0
00195,MACLISP
(DEFUN GENERATE-ADD-FACT-PART 101
(DEFUN GENERATE-ADD-SUB-FACT1 3405
(DEFUN GENERATE-SUB-FACT-PART 5205
(DEFUN GENERATE-UNDO-TUPLE-PART 6755
∨
AUX:<CL.THM>EVENTS.LISP.0
00290,MACLISP
(DEFEVENT ADD-AXIOM 90
(DEFEVENT ADD-SHELL667
(DEFUN BOOT-STRAP 1995
(DEFEVENT DCL 3205
(DEFEVENT DEFN 3557
(DEFEVENT DISABLE 4904
(DEFEVENT ENABLE 4997
(DEFEVENT PROVE-LEMMA 5097
(DEFEVENT REFLECT 6395
(DEFEVENT TOGGLE 8042
∨
AUX:<CL.THM>CODE-1-A.LISP.0
02649,MACLISP
(DEFUN 1ADD1 85
(DEFUN 1AND 166
(DEFUN 1APLY 226
(DEFUN 1CONS 573
(DEFUN 1COUNT 611
(DEFUN 1DIFFERENCE 1042
(DEFUN 1EQUAL 1153
(DEFUN 1FALSE 1213
(DEFUN 1FALSEP 1239
(DEFUN 1FIX 1293
(DEFUN 1IMPLIES 1371
(DEFUN 1LESSP 1423
(DEFUN 1LISTP 1497
(DEFUN 1LITATOM 1604
(DEFUN 1MINUS 1789
(DEFUN 1NEGATIVE-GUTS 1922
(DEFUN 1NEGATIVEP 2005
(DEFUN 1NLISTP 2179
(DEFUN 1NOT 2288
(DEFUN 1NUMBERP 2326
(DEFUN 1OR 2398
(DEFUN 1PACK 2446
(DEFUN 1PLUS 2669
(DEFUN 1QUOTIENT 2726
(DEFUN 1REMAINDER 2827
(DEFUN 1SUB1 2931
(DEFUN 1TIMES 3012
(DEFUN 1TRUE 3061
(DEFUN 1TRUEP 3086
(DEFUN 1UNPACK 3138
(DEFUN 1ZERO 3396
(DEFUN 1ZEROP 3420
(DEFUN ABBREVIATIONP 3522
(DEFUN ABBREVIATIONP1 3965
(DEFUN ACCEPTABLE-TYPE-PRESCRIPTION-LEMMAP 4274
(DEFUN ACCESS-ERROR 10255
(DEFUN ADD-AXIOM1 10440
(DEFUN ADD-DCELL 11167
(DEFUN ADD-ELIM-LEMMA 11297
(DEFUN ADD-EQUATION 11854
(DEFUN ADD-EQUATIONS 15681
(DEFUN ADD-EQUATIONS-TO-POT-LST 16589
(DEFUN ADD-FACT 19509
(DEFUN ADD-GENERALIZE-LEMMA 19639
(DEFUN ADD-LEMMA 19769
(DEFUN ADD-LEMMA0 19904
(DEFUN ADD-LESSP-ASSUMPTION-TO-POLY 20266
(DEFUN ADD-LINEAR-TERM 21178
(DEFUN ADD-LINEAR-VARIABLE 22979
(DEFUN ADD-LINEAR-VARIABLE1 23552
(DEFUN ADD-LITERAL 24157
(DEFUN ADD-META-LEMMA 24758
(DEFUN ADD-NOT-EQUAL-0-ASSUMPTION-TO-POLY 25054
(DEFUN ADD-NOT-LESSP-ASSUMPTION-TO-POLY 26327
(DEFUN ADD-NUMBERP-ASSUMPTION-TO-POLY 27796
(DEFUN ADD-PROCESS-HIST 29742
(DEFUN ADD-REWRITE-LEMMA 29945
(DEFUN ADD-SHELL-ROUTINES 31504
(DEFUN ADD-SHELL0 34371
(DEFUN ADD-SUB-FACT 40470
(DEFUN ADD-TERM-TO-POT-LST 44921
(DEFUN ADD-TERMS-TO-POT-LST 45345
(DEFUN ADD-TO-SET-EQ 49778
(DEFUN ADD-TYPE-SET-LEMMAS49864
(DEFUN ALL-ARGLISTS 51405
(DEFUN ALL-FNNAMES 52345
(DEFUN ALL-FNNAMES-LST 52418
(DEFUN ALL-FNNAMES1 52517
(DEFUN ALL-FNNAMES1-EVG 52848
(DEFUN ALL-INSERTIONS 53469
(DEFUN ALL-PATHS 53814
(DEFUN ALL-PERMUTATIONS 58075
(DEFUN ALL-PICKS 58288
(DEFUN ALL-SUBSEQUENCES 58645
(DEFUN ALL-VARS 59002
(DEFUN ALL-VARS-BAG 59195
(DEFUN ALL-VARS-BAG1 59264
(DEFUN ALL-VARS-LST 59434
(DEFUN ALL-VARS1 59583
(DEFUN ALMOST-SUBSUMES 59758
(DEFUN ALMOST-SUBSUMES-LOOP 60095
(DEFUN ALMOST-VALUEP 60802
(DEFUN ALMOST-VALUEP1 60881
(DEFUN APLY-SIMPLIFIER 61066
(DEFUN APPLY-HINTS 61412
(DEFUN APPLY-INDUCT-HINT 61841
(DEFUN APPLY-USE-HINT 62684
(DEFUN ARG1-IN-ARG2-UNIFY-SUBST 63432
(DEFUN ARGN0 63643
(DEFUN ARITY 64240
(DEFUN ASSOC-OF-APPEND 64436
(DEFUN ASSUME-TRUE-FALSE 64735
(DEFUN ATTEMPT-TO-REWRITE-RECOGNIZER 68150
∨
AUX:<CL.THM>CODE-B-D.LISP.0
03046,MACLISP
(DEFUN BATCH-PROVEALL 94
(DEFUN BOOLEAN 268
(DEFUN BOOT-STRAP0 344
(DEFUN BREAK-LEMMA 477
(DEFUN BTM-OBJECT 985
(DEFUN BTM-OBJECT-OF-TYPE-SET 1409
(DEFUN BTM-OBJECTP 1770
(DEFUN BUILD-SUM 2057
(DEFUN CANCEL 2449
(DEFUN CANCEL-POSITIVE 3541
(DEFUN CANCEL1 4213
(DEFUN CAR-CDRP 4989
(DEFUN CDR-ALL 5310
(DEFUN CHK-ACCEPTABLE-DEFN 5381
(DEFUN CHK-ACCEPTABLE-DCL 6869
(DEFUN CHK-ACCEPTABLE-ELIM-LEMMA 7345
(DEFUN CHK-ACCEPTABLE-GENERALIZE-LEMMA10291
(DEFUN CHK-ACCEPTABLE-HINTS 10361
(DEFUN CHK-ACCEPTABLE-LEMMA 14069
(DEFUN CHK-ACCEPTABLE-META-LEMMA 14809
(DEFUN CHK-ACCEPTABLE-REFLECT16934
(DEFUN CHK-ACCEPTABLE-REWRITE-LEMMA 18640
(DEFUN CHK-ACCEPTABLE-SHELL26075
(DEFUN CHK-ACCEPTABLE-TOGGLE 31667
(DEFUN CHK-ARGLIST 31995
(DEFUN CHK-MEANING 32516
(DEFUN CHK-NEW-1NAME 32923
(DEFUN CHK-NEW-NAME 33658
(DEFUN CLAUSIFY 34806
(DEFUN CLAUSIFY-INPUT 34999
(DEFUN CLAUSIFY-INPUT1 35282
(DEFUN CLEAN-UP-BRANCHES 36465
(DEFUN CNF-DNF 36749
(DEFUN COMMON-SWEEP 38077
(DEFUN COMMUTE-EQUALITIES 38895
(DEFUN COMPARE-STATS 39195
(DEFUN COMPLEMENTARY-MULTIPLEP 43577
(DEFUN COMPLEMENTARYP 44494
(DEFUN COMPLEXITY 44785
(DEFUN COMPRESS-POLY 45135
(DEFUN COMPRESS-POLY1 45365
(DEFUN COMPUTE-VETOES 45534
(DEFUN COMSUBT1 48995
(DEFUN COMSUBTERMS 51104
(DEFUN CONJOIN 51471
(DEFUN CONJOIN-CLAUSE-SETS 51630
(DEFUN CONJOIN2 51944
(DEFUN CONS-PLUS 52538
(DEFUN CONS-TERM 52652
(DEFUN CONSJOIN 54135
(DEFUN CONTAINS-REWRITEABLE-CALLP 54304
(DEFUN CONVERT-CAR-CDR 54734
(DEFUN CONVERT-CONS 55087
(DEFUN CONVERT-FOR 55231
(DEFUN CONVERT-NOT 55933
(DEFUN CONVERT-QUOTE 56068
(DEFUN CONVERT-TYPE-NO-TO-RECOGNIZER-TERM 56480
(DEFUN COUNT 56957
(DEFUN COUNT-IFS 57182
(DEFUN CREATE-REWRITE-RULE 57426
(DEFUN DCL0 57581
(DEFUN DECODE-IDATE 57788
(DEFUN DEFN-ASSUME-TRUE-FALSE 57845
(DEFUN DEFN-LOGIOR 61709
(DEFUN DEFN-SETUP 61798
(DEFUN DEFN-TYPE-SET 62471
(DEFUN DEFN-TYPE-SET2 63505
(DEFUN DEFN-WRAPUP 63595
(DEFUN DEFN0 64293
(DEFUN DELETE1 76574
(DEFUN DELETE-TAUTOLOGIES 76706
(DEFUN DELETE-TOGGLES 76967
(DEFUN DEPEND 77263
(DEFUN DEPENDENT-EVENTS 78080
(DEFUN DEPENDENTS-OF 78185
(DEFUN DEPENDENTS-OF1 78619
(DEFUN DESTRUCTORS 78950
(DEFUN DESTRUCTORS1 79194
(DEFUN DETACH 79506
(DEFUN DETACHED-ERROR 79628
(DEFUN DETACHEDP 79776
(DEFUN DISJOIN 79803
(DEFUN DISJOIN-CLAUSES 79933
(DEFUN DISJOIN2 80206
(DEFUN DTACK-0-ON-END 80850
(DEFUN DUMB-CONVERT-TYPE-SET-TO-TYPE-RESTRICTION-TERM 80937
(DEFUN DUMB-IMPLICATE-LITS 81810
(DEFUN DUMB-NEGATE-LIT 82116
(DEFUN DUMB-OCCUR 82529
(DEFUN DUMB-OCCUR-LST 82690
(DEFUN DUMP 82768
(DEFUN DUMP-ADD-AXIOM 84052
(DEFUN DUMP-ADD-SHELL 84547
(DEFUN DUMP-BEGIN-GROUP 86009
(DEFUN DUMP-DCL 86187
(DEFUN DUMP-DEFN 86558
(DEFUN DUMP-END-GROUP 87491
(DEFUN DUMP-HINTS 87689
(DEFUN DUMP-LEMMA-TYPES 89907
(DEFUN DUMP-OTHER 90326
(DEFUN DUMP-PROVE-LEMMA 90644
(DEFUN DUMP-TOGGLE 91166
∨
AUX:<CL.THM>CODE-E-M.LISP.0
03853,MACLISP
(DEFUN ELIMINABLE-VAR-CANDS 100
(DEFUN ELIMINABLEP 200
(DEFUN ELIMINATE-DESTRUCTORS-CANDIDATEP 647
(DEFUN ELIMINATE-DESTRUCTORS-CANDIDATES 2322
(DEFUN ELIMINATE-DESTRUCTORS-CANDIDATES1 2725
(DEFUN ELIMINATE-DESTRUCTORS-CLAUSE 3288
(DEFUN ELIMINATE-DESTRUCTORS-CLAUSE1 8164
(DEFUN ELIMINATE-DESTRUCTORS-SENT 8606
(DEFUN ELIMINATE-IRRELEVANCE-CLAUSE 8769
(DEFUN ELIMINATE-IRRELEVANCE-SENT 9559
(DEFUN EQUATIONAL-PAIR-FOR 9706
(DEFUN ERASE-EOL 9906
(DEFUN ERASE-EOP 9956
(DEFUN ERROR1 10003
(DEFUN EVENT-FORM 10998
(DEFUN EVENT1-OCCURRED-BEFORE-EVENT2 11200
(DEFUN EVENTS-SINCE 11318
(DEFUN EVG 11522
(DEFUN EVG-OCCUR-LEGAL-CHAR-CODE-SEQ 12688
(DEFUN EVG-OCCUR-NUMBER 13324
(DEFUN EVG-OCCUR-OTHER 13904
(DEFUN EXECUTE 14251
(DEFUN EXPAND-ABBREVIATIONS 14607
(DEFUN EXPAND-AND-ORS 16383
(DEFUN EXPAND-BOOT-STRAP-NON-REC-FNS 17946
(DEFUN EXPAND-NON-REC-FNS 18424
(DEFUN EXPAND-PPR-MACROS 18860
(DEFUN EXTEND-ALIST 21181
(DEFUN EXTERNAL-LINEARIZE 21451
(DEFUN EXTRACT-DEPENDENCIES-FROM-HINTS 21594
(DEFUN FALSE-NONFALSEP 21902
(DEFUN FAVOR-COMPLICATED-CANDIDATES 22267
(DEFUN FERTILIZE-CLAUSE 22563
(DEFUN FERTILIZE-FEASIBLE 24495
(DEFUN FERTILIZE-SENT 24946
(DEFUN FERTILIZE1 25085
(DEFUN FILTER-ARGS 25464
(DEFUN FIND-EQUATIONAL-POLY 25657
(DEFUN FIRST-COEFFICIENT 27992
(DEFUN FIRST-VAR 28063
(DEFUN FITS 28129
(DEFUN FIXCAR-CDR 28467
(DEFUN FLATTEN-ANDS-IN-LIT 28732
(DEFUN FLESH-OUT-IND-PRIN29198
(DEFUN FLUSH-CAND1-DOWN-CAND2 30933
(DEFUN FN-SYMB0 32604
(DEFUN FNNAMEP 32926
(DEFUN FNNAMEP-IF 33209
(DEFUN FORM-COUNT 33390
(DEFUN FORM-COUNT-EVG 33640
(DEFUN FORM-COUNT1 34415
(DEFUN FORM-INDUCTION-CLAUSE 34664
(DEFUN FORMP-SIMPLIFIER 35494
(DEFUN FORMULA-OF 36424
(DEFUN FREE-VAR-CHK 36610
(DEFUN FREE-VARSP 37392
(DEFUN GEN-VARS 37569
(DEFUN GENERALIZE-CLAUSE 37865
(DEFUN GENERALIZE-SENT 38592
(DEFUN GENERALIZE1 38739
(DEFUN GENERALIZE2 39156
(DEFUN GENRLT1 39440
(DEFUN GENRLTERMS 39737
(DEFUN GET-CANDS 39806
(DEFUN GET-LISP-SEXPR 40151
(DEFUN GET-LEVEL-NO 40734
(DEFUN GET-STACK-NAME 40810
(DEFUN GET-STACK-NAME1 40987
(DEFUN GET-TYPES 41245
(DEFUN GREATEREQP 42526
(DEFUN GUARANTEE-CITIZENSHIP 42583
(DEFUN GUESS-RELATION-MEASURE-LST 42897
(DEFUN HAS-LIB-PROPS 43402
(DEFUN ILLEGAL-CALL 43553
(DEFUN ILLEGAL-NAME 43711
(DEFUN IMMEDIATE-DEPENDENTS-OF 43854
(DEFUN IMPLIES? 47052
(DEFUN IMPOSSIBLE-POLYP 47116
(DEFUN IND-FORMULA 47292
(DEFUN INDUCT 50194
(DEFUN INDUCT-VARS 52111
(DEFUN INDUCTION-MACHINE 52788
(DEFUN INFORM-SIMPLIFY 53511
(DEFUN INIT-LEMMA-STACK 56033
(DEFUN INIT-LIB 56097
(DEFUN INIT-LINEARIZE-ASSUMPTIONS-STACK 56438
(DEFUN INTERESTING-SUBTERMS 56552
(DEFUN INTERSECTP 57130
(DEFUN INTRODUCE-ANDS 57201
(DEFUN INTRODUCE-LISTS 57877
(DEFUN JUMPOUTP 58442
(DEFUN KILL-EVENT 61444
(DEFUN KILL-LIB 61810
(DEFUN KILLPROPLIST1 62306
(DEFUN LEGAL-CHAR-CODE-SEQ 62503
(DEFUN LENGTH-TO-ATOM 63031
(DEFUN LESSEQP 63104
(DEFUN LEXORDER 63148
(DEFUN LINEARIZE 63662
(DEFUN LISTABLE 67445
(DEFUN LOGSUBSETP 67728
(DEFUN LOOKUP-HYP 67775
(DEFUN LOOP-STOPPER 69307
(DEFUN MAIN-EVENT-OF 69607
(DEFUN MAKE-EVENT 70001
(DEFUN MAKE-FLATTENED-MACHINE 70195
(DEFUN MAKE-NEW-NAME 71296
(DEFUN MAKE-REWRITE-RULES 71458
(DEFUN MAKE-TYPE-RESTRICTION 72406
(DEFUN MAX-FORM-COUNT 73183
(DEFUN MAXIMAL-ELEMENTS 73870
(DEFUN MEANING-SIMPLIFIER 74152
(DEFUN MEMB-NEGATIVE 79930
(DEFUN MENTIONSQ 80057
(DEFUN MENTIONSQ-LST 80201
(DEFUN MERGE-CAND1-INTO-CAND2 80368
(DEFUN MERGE-CANDS 83030
(DEFUN MERGE-DESTRUCTOR-CANDIDATES 83260
(DEFUN MERGE-TESTS-AND-ALISTS 83618
(DEFUN MERGE-TESTS-AND-ALISTS-LSTS84407
(DEFUN META-LEMMAP 86067
(DEFUN MULTIPLE-PIGEON-HOLE 86140
∨
AUX:<CL.THM>CODE-N-R.LISP.0
03461,MACLISP
(DEFUN NEGATE 86
(DEFUN NEGATE-LIT 638
(DEFUN NEXT-AVAILABLE-TYPE-NO 905
(DEFUN NO-CROWDINGP 1567
(DEFUN NO-DUPLICATESP 1811
(DEFUN NO-OP 1891
(DEFUN NON-RECURSIVE-DEFNP 1930
(DEFUN NORMALIZE-IFS 2146
(DEFUN NOT-EQUAL-0? 4057
(DEFUN NOT-IDENT 4566
(DEFUN NOT-LESSP? 5090
(DEFUN NOT-TO-BE-REWRITTENP 5466
(DEFUN NUMBERP? 6693
(DEFUN OBJ-TABLE 6925
(DEFUN OCCUR 7592
(DEFUN OCCUR-CNT 8160
(DEFUN OCCUR-LST 8461
(DEFUN ONE-WAY-UNIFY 8534
(DEFUN ONE-WAY-UNIFY-LIST 8636
(DEFUN ONE-WAY-UNIFY1 8870
(DEFUN ONE-WAY-UNIFY11 9091
(DEFUN ONEIFY 10210
(DEFUN ONEIFY-ASSUME-FALSE 11407
(DEFUN ONEIFY-ASSUME-TRUE 11486
(DEFUN ONEIFY-TEST 11821
(DEFUN OPTIMIZE-COMMON-SUBTERMS 13277
(DEFUN PARTITION 18334
(DEFUN PARTITION-CLAUSES 18691
(DEFUN PATH-ADD-TO-SET 19759
(DEFUN PATH-EQ 19860
(DEFUN PATH-POT-SUBSUMES 19986
(DEFUN PATH-UNION 20186
(DEFUN PEGATE-LIT 20337
(DEFUN PETITIO-PRINCIPII 20472
(DEFUN PICK-HIGH-SCORES 20948
(DEFUN PIGEON-HOLE 21151
(DEFUN PIGEON-HOLE-IN-ALL-POSSIBLE-WAYS 21520
(DEFUN PIGEON-HOLE1 22282
(DEFUN PLUSJOIN 22979
(DEFUN POLY-MEMBER 23155
(DEFUN POP-CLAUSE-SET 23390
(DEFUN POP-LEMMA-FRAME 24602
(DEFUN POP-LINEARIZE-ASSUMPTIONS-FRAME 24889
(DEFUN POPU 25262
(DEFUN POSSIBLE-IND-PRINCIPLES 25424
(DEFUN POSSIBLY-NUMERIC 26241
(DEFUN POWER-EVAL 26381
(DEFUN POWER-REP 26489
(DEFUN PPC 26611
(DEFUN PPE 26673
(DEFUN PPE-LST 26715
(DEFUN PPR 27174
(DEFUN PPRINDENT 27290
(DEFUN PPSD 27529
(DEFUN PPSD-LST 27573
(DEFUN PREPROCESS 27764
(DEFUN PREPROCESS-HYPS 28069
(DEFUN PRETTYIFY-CLAUSE 28507
(DEFUN PRETTYIFY-LISP 28878
(DEFUN PRIMITIVE-RECURSIVEP 28968
(DEFUN PRIMITIVEP 29379
(DEFUN PRINT-IDATE 29670
(DEFUN PRINT-STACK 30275
(DEFUN PRINT-STATS 30361
(DEFUN PRINT-TO-DISPLAY 30609
(DEFUN PROCESS-EQUATIONAL-POLYS 31459
(DEFUN PROPERTYLESS-SYMBOLP 33270
(DEFUN PROVE 33374
(DEFUN PROVE-TERMINATION 33979
(DEFUN PROVEALL 34593
(DEFUN PUSH-CLAUSE-SET 35094
(DEFUN PUSH-LEMMA 35202
(DEFUN PUSH-LEMMA-FRAME 35349
(DEFUN PUSH-LINEARIZE-ASSUMPTION 35605
(DEFUN PUSH-LINEARIZE-ASSUMPTIONS-FRAME 35757
(DEFUN PUSHU 36107
(DEFUN PUT-CURSOR 36232
(DEFUN PUT-INDUCTION-INFO 36287
(DEFUN PUT-LEVEL-NO 38112
(DEFUN PUT-TYPE-PRESCRIPTION 38500
(DEFUN PUT0 42209
(DEFUN PUT00 43800
(DEFUN PUT1 44158
(DEFUN PUT1-LST 44962
(DEFUN PUTD1 45194
(DEFUN QUICK-BLOCK-INFO 45718
(DEFUN QUICK-BLOCK-INFO1 46692
(DEFUN QUICK-WORSE-THAN 46853
(DEFUN R 47657
(DEFUN REDO! 47871
(DEFUN REDO-UNDONE-EVENTS47995
(DEFUN REDO-UNDONE-EVENTS-APPLY 51411
(DEFUN REDUCE 51500
(DEFUN REDUCE1 51926
(DEFUN REFLECT0 53068
(DEFUN RELIEVE-HYPS 55085
(DEFUN RELIEVE-HYPS-NOT-OK 55465
(DEFUN RELIEVE-HYPS1 55943
(DEFUN REMOVE-2IFS 57966
(DEFUN REMOVE-NEGATIVE 58496
(DEFUN REMOVE-REDUNDANT-TESTS 58661
(DEFUN REMOVE1 60028
(DEFUN REMOVE-TRIVIAL-EQUATIONS 60175
(DEFUN REMOVE-UNCHANGING-VARS 61287
(DEFUN REMPROP1 61851
(DEFUN RESTART 62058
(DEFUN RESTART-BATCH 62183
(DEFUN REWRITE 62428
(DEFUN REWRITE-FNCALL 64623
(DEFUN REWRITE-FNCALLP 69114
(DEFUN REWRITE-FOR 70618
(DEFUN REWRITE-IF 70845
(DEFUN REWRITE-IF1 71706
(DEFUN REWRITE-LINEAR-CONCL 72055
(DEFUN REWRITE-SOLIDIFY 73655
(DEFUN REWRITE-TYPE-PRED 74557
(DEFUN REWRITE-WITH-LEMMAS 77836
(DEFUN REWRITE-WITH-LINEAR 84664
(DEFUN RPLACAI 86592
∨
AUX:<CL.THM>CODE-S-Z.LISP.0
03015,MACLISP
(DEFUN S 81
(DEFUN SARGS 528
(DEFUN SCONS-TERM 1228
(DEFUN SCRUNCH 1496
(DEFUN SCRUNCH-CLAUSE 1619
(DEFUN SCRUNCH-CLAUSE-SET 1814
(DEFUN SEARCH-GROUND-UNITS 2067
(DEFUN SEQUENTIAL-DIFFERENCE 3129
(DEFUN SET-DIFF 3531
(DEFUN SET-DIFF-N 3616
(DEFUN SET-EQUAL 3984
(DEFUN SET-SIMPLIFY-CLAUSE-POT-LST 4074
(DEFUN SETTLED-DOWN-CLAUSE 6067
(DEFUN SETTLED-DOWN-SENT 6249
(DEFUN SETUP 6392
(DEFUN SETUP-META-NAMES 7163
(DEFUN SHELL-CONSTRUCTORP 7477
(DEFUN SHELL-DESTRUCTOR-NESTP 7598
(DEFUN SHELL-OCCUR 7860
(DEFUN SHELL-OCCUR1 9098
(DEFUN SHELLP 10739
(DEFUN SIMPLIFY-CLAUSE 10940
(DEFUN SIMPLIFY-CLAUSE-MAXIMALLY 14908
(DEFUN SIMPLIFY-CLAUSE-MAXIMALLY1 15253
(DEFUN SIMPLIFY-CLAUSE0 15704
(DEFUN SIMPLIFY-CLAUSE1 16914
(DEFUN SIMPLIFY-LOOP 18957
(DEFUN SIMPLIFY-SENT 19361
(DEFUN SINGLETON-CONSTRUCTOR-TO-RECOGNIZER 19521
(DEFUN SKO-DEST-NESTP 19843
(DEFUN SOME-SUBTERM-WORSE-THAN-OR-EQUAL 20284
(DEFUN SORT-DESTRUCTOR-CANDIDATES 20686
(DEFUN SOUND-IND-PRIN-MASK 21798
(DEFUN STACK-DEPTH 25762
(DEFUN START-STATS 25839
(DEFUN STOP-STATS 25928
(DEFUN STORE-SENT 26154
(DEFUN STRIP-BRANCHES 27877
(DEFUN STRIP-BRANCHES1 28195
(DEFUN SUB-SEQUENCEP 31356
(DEFUN SUBBAGP 31584
(DEFUN SUBLIS-EXPR 31776
(DEFUN SUBLIS-EXPR1 31942
(DEFUN SUBLIS-VAR 32215
(DEFUN SUBLIS-VAR-LST 32670
(DEFUN SUB-PAIR-EXPR 32773
(DEFUN SUB-PAIR-EXPR-LST 32940
(DEFUN SUB-PAIR-EXPR1 33049
(DEFUN SUB-PAIR-VAR 33449
(DEFUN SUB-PAIR-VAR-LST 33866
(DEFUN SUBSETP 33967
(DEFUN SUBST-EXPR 34040
(DEFUN SUBST-EXPR-ERROR1 34218
(DEFUN SUBST-EXPR-LST 34507
(DEFUN SUBST-EXPR1 34598
(DEFUN SUBST-FN 34841
(DEFUN SUBST-VAR 35322
(DEFUN SUBST-VAR-LST 35583
(DEFUN SUBSTITUTE 35686
(DEFUN SUBSUMES 35809
(DEFUN SUBSUMES-REWRITE-RULE 35896
(DEFUN SUBSUMES1 36202
(DEFUN SUBSUMES11 36365
(DEFUN SUM-STATS-ALIST 36494
(DEFUN SWAP-OUT 36624
(DEFUN TABULATE 36698
(DEFUN TERM-ORDER 36778
(DEFUN TERMINATION-MACHINE 40003
(DEFUN TERMP 41203
(DEFUN TP-EXPLODEN1 41908
(DEFUN TP-GETCHARN1 42306
(DEFUN TP-IMPLODE1 42694
(DEFUN TO-BE-IGNOREDP 43257
(DEFUN TOO-MANY-IFS 43513
(DEFUN TOP-FNNAME 46574
(DEFUN TOTAL-FUNCTIONP 46739
(DEFUN TRANSITIVE-CLOSURE 46976
(DEFUN TRANSLATE 48257
(DEFUN TRANSLATE-LOOP←FOR 53086
(DEFUN TRANSLATE-TO-LISP 54975
(DEFUN TREE-DEPENDENTS 55297
(DEFUN TRIVIAL-POLYP 55532
(DEFUN TRIVIAL-POLYP1 55658
(DEFUN TRUE-POLYP 57586
(DEFUN TYPE-ALIST-CLAUSE 57767
(DEFUN TYPE-PRESCRIPTION-LEMMAP 58092
(DEFUN TYPE-SET 58319
(DEFUN TYPE-SET2 60059
(DEFUN UBT 60262
(DEFUN UNBREAK-LEMMA 60330
(DEFUN UNCHANGING-VARS 60504
(DEFUN UNCHANGING-VARS1 60613
(DEFUN UNDO-BACK-THROUGH 61262
(DEFUN UNDO-NAME 61630
(DEFUN UNION-EQUAL 62203
(DEFUN UNPRETTYIFY 62989
(DEFUN VARIANTP 63610
(DEFUN WORSE-THAN 63827
(DEFUN WORSE-THAN-OR-EQUAL 64071
(DEFUN WRAPUP 64163
(DEFUN XXXJOIN 64853
(DEFUN ZERO-POLY 65189
∨
AUX:<CL.THM>IO.LISP.0
00599,MACLISP
(DEFUN !CLAUSE-SET 85
(DEFUN !CLAUSE 537
(DEFUN EQUALITY-HYP-NO 808
(DEFUN GET-SCHEMA-MEASURE-RELATION 1087
(DEFUN IO 2428
(DEFUN IO1 2666
(DEFUN JUSTIFICATION-SENTENCE 29511
(DEFUN !LIST 30944
(DEFUN MAPRINEVAL 31122
(DEFUN NOTICE-CLAUSE 31605
(DEFUN PEVAL 31739
(DEFUN PEVAL-APPLY 32437
(DEFUN PEVALV 32945
(DEFUN PLURALP 33206
(DEFUN !PPR-LIST 33296
(DEFUN !PPR 33550
(DEFUN PRIN5* 34528
(DEFUN PRINEVAL 36399
(DEFUN PRINEVAL1 36471
(DEFUN PRINT-DEFN-MSG 37246
(DEFUN TH-IFY 41083
(DEFUN UN-NOTICE-CLAUSE 41697
∨
AUX:<CL.THM>PPR.LISP.0
00168,MACLISP
(DEFUN PPRIND 295
(DEFUN PPRPACK 977
(DEFUN PPR1 1145
(DEFUN PPR2 4755
(DEFUN PPR22 7600
(DEFUN TERPRISPACES 8201
∨
AUX:<CL.THM>TOPS-20-EMACS-TO-THM.LISP.0
00408,MACLISP
(DEFVAR FORMS)47
(DEFVAR DRIBBLE-FILE 72
(DEFVAR EMACS-FORK-NAME 131
(DEFVAR EMACS-FORK-NAME-COPY)178
(DEFVAR EMACS-TO-THM-STRING)210
(DEFUN SET-EMACS-TO-THM-STRING 245
(DEFUN DRIBBLE-START 537
(DEFUN DRIBBLE-PAUSE 1008
(DEFUN DRIBBLE-END 1342
(DEFUN EMACS-TO-THM-P 1550
(DEFUN EMACS-TO-THM-Y 1998
(DEFUN EMACS-TO-THM-E 2511
∨